package kodkod.analysis;

import java.util.*;

import kodkod.ast.*;
import kodkod.ast.operator.ExprCastOperator;
import kodkod.ast.operator.IntOperator;
import kodkod.instance.TupleSet;

public class Casts extends HashSet<Expression> {
	
	public static boolean includeSumCasts = false;
	public static boolean includeNegCasts = false;
	
	ArrayList<IfIntExpression> ifIntExpressions = new ArrayList<IfIntExpression>();
	
	public Casts(IntExpression exp) {
		super();
		
		if (exp instanceof UnaryIntExpression) {
			UnaryIntExpression e = (UnaryIntExpression)exp;
			Casts child = new Casts(e.intExpr());
			if (includeNegCasts || !e.op().equals(IntOperator.NEG)) {
				this.addAll(child);
			}
			this.ifIntExpressions.addAll(child.ifIntExpressions);
		} else if (exp instanceof BinaryIntExpression) {
			BinaryIntExpression e = (BinaryIntExpression)exp;
			Casts left = new Casts(e.left());
			Casts right = new Casts(e.right());
			this.addAll(left);
			if (includeNegCasts || !e.op().equals(IntOperator.MINUS)) {
				this.addAll(right);
			}
			this.ifIntExpressions.addAll(left.ifIntExpressions);
			this.ifIntExpressions.addAll(right.ifIntExpressions);
		} else if (exp instanceof NaryIntExpression) {
			NaryIntExpression e = (NaryIntExpression)exp;
			for (IntExpression ce : e) {
				Casts child = new Casts(ce);
				this.addAll(child);
				this.ifIntExpressions.addAll(child.ifIntExpressions);
			}
		} else if (exp instanceof SumExpression) {
			SumExpression e = (SumExpression)exp;
			Casts child = new Casts(e.intExpr());
			this.addAll(child);
			this.ifIntExpressions.addAll(child.ifIntExpressions);
		} else if (exp instanceof IfIntExpression) {
			IfIntExpression e = (IfIntExpression)exp;
			Casts thenExpr = new Casts(e.thenExpr());
			Casts elseExpr = new Casts(e.elseExpr());
			this.addAll(thenExpr);
			this.addAll(elseExpr);
			ifIntExpressions.addAll(thenExpr.ifIntExpressions);
			ifIntExpressions.addAll(elseExpr.ifIntExpressions);
		} else if (exp instanceof ExprToIntCast) {
			ExprToIntCast e = (ExprToIntCast)exp;
			if (e.op().equals(ExprCastOperator.CARDINALITY)) {
				this.add(e.expression());
			} else if (includeSumCasts) {
				this.add(e.expression());
			}
		} 
	}
}
